the proof LISPAX:

(DECL (U U0 U1 U2 U3 V V0 V1 V2 V3 W W0 W1 W2 W3) |GROUND| VARIABLE LISTP)

(DECL (X Y Z) |GROUND| VARIABLE SEXP)

(DECL (A B C) |GROUND| VARIABLE)

(DECL (PHI) |GROUND→TRUTHVAL| VARIABLE)

(DECL (NNIL) |GROUND| CONSTANT LISTP)

(DECL (CONS) |GROUND⊗GROUND→GROUND| CONSTANT)

(DECL (CAR CDR) |GROUND→GROUND| CONSTANT)

(DECL (NULL) |GROUND→TRUTHVAL| CONSTANT)

(DECL (LISTP) |GROUND→TRUTHVAL| CONSTANT)

(DECL (SEXP) |GROUND→TRUTHVAL| CONSTANT)

(AXIOM |∀U.SEXP(U)|)
11. ∀U.SEXP(U)
    ctxt: (1 10)   deps: NIL

(AXIOM |∀X U.LISTP(CONS(X,U))|)
12. ∀X U.LISTP(CONS(X,U))
    ctxt: (1 2 6 9)   deps: NIL

(AXIOM |∀U.NULL(U)≡U=NNIL|)
13. ∀U.NULL(U)≡U=NNIL
    ctxt: (1 5 8)   deps: NIL

(AXIOM |∀X U.¬NULL(CONS(X,U))|)
14. ∀X U.¬NULL(CONS(X,U))
    ctxt: (1 2 6 8)   deps: NIL

(AXIOM |∀X U.CAR(CONS(X,U))=X|)
15. ∀X U.CAR(CONS(X,U))=X
    ctxt: (1 2 6 7)   deps: NIL

(AXIOM |∀X U.CDR(CONS(X,U))=U|)
16. ∀X U.CDR(CONS(X,U))=U
    ctxt: (1 2 6 7)   deps: NIL

(AXIOM |∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(CONS(X,U)))⊃(∀U.PHI(U))|)
17. ∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(CONS(X,U)))⊃(∀U.PHI(U))
    ctxt: (1 2 4 5 6)   deps: NIL

(DECL (*) |GROUND⊗GROUND→GROUND| CONSTANT NIL INFIX 840)

(AXIOM |∀U V.LISTP(U*V)|)
19. ∀U V.LISTP(U*V)
    ctxt: (1 9 18)   deps: NIL

(AXIOM |∀U V.U*V=IF NULL(U) THEN V ELSE CONS(CAR(U),CDR(U)*V)|)
20. ∀U V.U*V=IF NULL(U) THEN V ELSE CONS(CAR(U),CDR(U)*V)
    ctxt: (1 6 7 8 18)   deps: NIL

(DECL (REVERSE LIST1) |GROUND→GROUND| CONSTANT)

(DECL (LIST) |(GROUND*→GROUND)| FUNCTIONAL)

(AXIOM |∀X.LISTP(LIST(X))|)
23. ∀X.LISTP(LIST(X))
    ctxt: (2 9 22)   deps: NIL

(AXIOM |∀X.LIST(X)=CONS(X,NNIL)|)
24. ∀X.LIST(X)=CONS(X,NNIL)
    ctxt: (2 5 6 22)   deps: NIL

(AXIOM |∀X Y.LISTP(LIST(X,Y))|)
25. ∀X Y.LISTP(LIST(X,Y))
    ctxt: (2 9 22)   deps: NIL

(AXIOM |∀X Y.LIST(X,Y)=CONS(X,LIST(Y))|)
26. ∀X Y.LIST(X,Y)=CONS(X,LIST(Y))
    ctxt: (2 6 22)   deps: NIL

(AXIOM |∀X Y Z.LISTP(LIST(X,Y,Z))|)
27. ∀X Y Z.LISTP(LIST(X,Y,Z))
    ctxt: (2 9 22)   deps: NIL

(AXIOM |∀X Y Z.LIST(X,Y,Z)=CONS(X,LIST(Y,Z))|)
28. ∀X Y Z.LIST(X,Y,Z)=CONS(X,LIST(Y,Z))
    ctxt: (2 6 22)   deps: NIL

(AXIOM |∀U.LISTP(REVERSE(U))|)
29. ∀U.LISTP(REVERSE(U))
    ctxt: (1 9 21)   deps: NIL

(AXIOM |∀U.REVERSE(U)=IF NULL(U) THEN NNIL ELSE REVERSE(CDR(U))*LIST(CAR(U))|)
30. ∀U.REVERSE(U)=IF NULL(U) THEN NNIL ELSE REVERSE(CDR(U))*LIST(CAR(U))
    ctxt: (1 5 7 8 18 21 22)   deps: NIL

(AXIOM |∀U V W.(U*V)*W=U*(V*W)|)
31. ∀U V W.(U*V)*W=U*(V*W)
    ctxt: (1 18)   deps: NIL

(AXIOM |∀X U V.CONS(X,U*V)=CONS(X,U)*V|)
32. ∀X U V.CONS(X,U*V)=CONS(X,U)*V
    ctxt: (1 2 6 18)   deps: NIL

(AXIOM |∀U V.REVERSE(U*V)=REVERSE(V)*REVERSE(U)|)
33. ∀U V.REVERSE(U*V)=REVERSE(V)*REVERSE(U)
    ctxt: (1 18 21)   deps: NIL